#ifndef LIT_UNION_H
#define LIT_UNION_H

#include "union.h"
#include "aig_phase.h"

class LitUnion
{
   Union        _varEq;
   public:
   AigPhase     _ph;

   LitUnion( StrashAIG & ckt) : _ph(ckt) {}
   ~LitUnion(){}

   void conjunct( unsigned a ,unsigned b){ _varEq.conjunct( a , b ); }

   AigLit eq( AigLit a ) const
   {
      unsigned eqvar = _varEq[ var(a) ];
      return toAigLit( eqvar , _ph[ var(a) ] ^ _ph[ eqvar ] ^ sign( a ) );
   }
   unsigned eqIdx( unsigned a )const{ return _varEq[ a ] ; }
   bool ph( unsigned i )       const{return _ph[i];}
   void init(){_ph.init();}
   void validation( unsigned s ){ _ph.validation() , _varEq.validation( s );}
};


#endif
